package test.cap.jeeves

import cap.scalasmt._
import cap.jeeves._
import org.scalatest.FunSuite
import org.scalatest.Assertions.{expectResult}
import scala.collection.immutable.Map
import cap.jeeves.JeevesTypes._

class ExampleJeevesLib extends FunSuite with JeevesLib {
  test ("sensitive int") {
    val l = mkLevel();
    val x = mkSensitiveInt(l, 42, -1);

    expectResult(42) {concretize(l === HIGH, x)};
    expectResult(-1) {concretize(l === LOW, x)};
  }

  test ("sensitive object") {
    val l = mkLevel();
    val t = Test(1);

    val x = mkSensitive(l, t, NULL);
    
    expectResult(t) {concretize(l === HIGH, x)};
    expectResult(null) {concretize(l === LOW, x)};
  }

  case class Test(id: Int) extends JeevesRecord
  test ("test restrict") {
    val x = Test(1)
    val a = mkLevel ()
    restrict (a, (ctxt: Sensitive) => ctxt === x)
    val xS = mkSensitive (a, x, Test(-1))
    expectResult (x) { concretize (x, xS) }
  }

  /*
  test ("concretizeList non-null") {
    val x = pickObject[Test];
    assume(x === Test(0));
    val symList = List(x);
    val cList : List[Test] = concretize(NULL, symList);
    expect(List(Test(0))) {cList};
  }
  */

  /*
  test ("concretizeList null") {
    val x = pickObject[Test](NULL);
    val symList = List(x);
    val cList : List[Test] = concretize(NULL, symList);
    expect(Nil) {cList};
  }
  */
}
